0 Prolog
↳1 PrologToPiTRSProof (⇒, 53 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 0 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 3 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 32 ms)
↳11 QDP
↳12 UsableRulesReductionPairsProof (⇔, 45 ms)
↳13 QDP
↳14 PisEmptyProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇒, 0 ms)
↳20 QDP
↳21 UsableRulesReductionPairsProof (⇔, 80 ms)
↳22 QDP
↳23 QReductionProof (⇔, 0 ms)
↳24 QDP
↳25 MRRProof (⇔, 40 ms)
↳26 QDP
↳27 DependencyGraphProof (⇔, 0 ms)
↳28 TRUE
count_in_ga(atom(X), s(0)) → count_out_ga(atom(X), s(0))
count_in_ga(cons(atom(X), Y), s(Z)) → U3_ga(X, Y, Z, count_in_ga(Y, Z))
count_in_ga(cons(cons(U, V), W), Z) → U4_ga(U, V, W, Z, flatten_in_ga(cons(cons(U, V), W), X))
flatten_in_ga(atom(X), .(X, [])) → flatten_out_ga(atom(X), .(X, []))
flatten_in_ga(cons(atom(X), U), .(X, Y)) → U1_ga(X, U, Y, flatten_in_ga(U, Y))
flatten_in_ga(cons(cons(U, V), W), X) → U2_ga(U, V, W, X, flatten_in_ga(cons(U, cons(V, W)), X))
U2_ga(U, V, W, X, flatten_out_ga(cons(U, cons(V, W)), X)) → flatten_out_ga(cons(cons(U, V), W), X)
U1_ga(X, U, Y, flatten_out_ga(U, Y)) → flatten_out_ga(cons(atom(X), U), .(X, Y))
U4_ga(U, V, W, Z, flatten_out_ga(cons(cons(U, V), W), X)) → U5_ga(U, V, W, Z, count_in_ga(X, Z))
U5_ga(U, V, W, Z, count_out_ga(X, Z)) → count_out_ga(cons(cons(U, V), W), Z)
U3_ga(X, Y, Z, count_out_ga(Y, Z)) → count_out_ga(cons(atom(X), Y), s(Z))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
count_in_ga(atom(X), s(0)) → count_out_ga(atom(X), s(0))
count_in_ga(cons(atom(X), Y), s(Z)) → U3_ga(X, Y, Z, count_in_ga(Y, Z))
count_in_ga(cons(cons(U, V), W), Z) → U4_ga(U, V, W, Z, flatten_in_ga(cons(cons(U, V), W), X))
flatten_in_ga(atom(X), .(X, [])) → flatten_out_ga(atom(X), .(X, []))
flatten_in_ga(cons(atom(X), U), .(X, Y)) → U1_ga(X, U, Y, flatten_in_ga(U, Y))
flatten_in_ga(cons(cons(U, V), W), X) → U2_ga(U, V, W, X, flatten_in_ga(cons(U, cons(V, W)), X))
U2_ga(U, V, W, X, flatten_out_ga(cons(U, cons(V, W)), X)) → flatten_out_ga(cons(cons(U, V), W), X)
U1_ga(X, U, Y, flatten_out_ga(U, Y)) → flatten_out_ga(cons(atom(X), U), .(X, Y))
U4_ga(U, V, W, Z, flatten_out_ga(cons(cons(U, V), W), X)) → U5_ga(U, V, W, Z, count_in_ga(X, Z))
U5_ga(U, V, W, Z, count_out_ga(X, Z)) → count_out_ga(cons(cons(U, V), W), Z)
U3_ga(X, Y, Z, count_out_ga(Y, Z)) → count_out_ga(cons(atom(X), Y), s(Z))
COUNT_IN_GA(cons(atom(X), Y), s(Z)) → U3_GA(X, Y, Z, count_in_ga(Y, Z))
COUNT_IN_GA(cons(atom(X), Y), s(Z)) → COUNT_IN_GA(Y, Z)
COUNT_IN_GA(cons(cons(U, V), W), Z) → U4_GA(U, V, W, Z, flatten_in_ga(cons(cons(U, V), W), X))
COUNT_IN_GA(cons(cons(U, V), W), Z) → FLATTEN_IN_GA(cons(cons(U, V), W), X)
FLATTEN_IN_GA(cons(atom(X), U), .(X, Y)) → U1_GA(X, U, Y, flatten_in_ga(U, Y))
FLATTEN_IN_GA(cons(atom(X), U), .(X, Y)) → FLATTEN_IN_GA(U, Y)
FLATTEN_IN_GA(cons(cons(U, V), W), X) → U2_GA(U, V, W, X, flatten_in_ga(cons(U, cons(V, W)), X))
FLATTEN_IN_GA(cons(cons(U, V), W), X) → FLATTEN_IN_GA(cons(U, cons(V, W)), X)
U4_GA(U, V, W, Z, flatten_out_ga(cons(cons(U, V), W), X)) → U5_GA(U, V, W, Z, count_in_ga(X, Z))
U4_GA(U, V, W, Z, flatten_out_ga(cons(cons(U, V), W), X)) → COUNT_IN_GA(X, Z)
count_in_ga(atom(X), s(0)) → count_out_ga(atom(X), s(0))
count_in_ga(cons(atom(X), Y), s(Z)) → U3_ga(X, Y, Z, count_in_ga(Y, Z))
count_in_ga(cons(cons(U, V), W), Z) → U4_ga(U, V, W, Z, flatten_in_ga(cons(cons(U, V), W), X))
flatten_in_ga(atom(X), .(X, [])) → flatten_out_ga(atom(X), .(X, []))
flatten_in_ga(cons(atom(X), U), .(X, Y)) → U1_ga(X, U, Y, flatten_in_ga(U, Y))
flatten_in_ga(cons(cons(U, V), W), X) → U2_ga(U, V, W, X, flatten_in_ga(cons(U, cons(V, W)), X))
U2_ga(U, V, W, X, flatten_out_ga(cons(U, cons(V, W)), X)) → flatten_out_ga(cons(cons(U, V), W), X)
U1_ga(X, U, Y, flatten_out_ga(U, Y)) → flatten_out_ga(cons(atom(X), U), .(X, Y))
U4_ga(U, V, W, Z, flatten_out_ga(cons(cons(U, V), W), X)) → U5_ga(U, V, W, Z, count_in_ga(X, Z))
U5_ga(U, V, W, Z, count_out_ga(X, Z)) → count_out_ga(cons(cons(U, V), W), Z)
U3_ga(X, Y, Z, count_out_ga(Y, Z)) → count_out_ga(cons(atom(X), Y), s(Z))
COUNT_IN_GA(cons(atom(X), Y), s(Z)) → U3_GA(X, Y, Z, count_in_ga(Y, Z))
COUNT_IN_GA(cons(atom(X), Y), s(Z)) → COUNT_IN_GA(Y, Z)
COUNT_IN_GA(cons(cons(U, V), W), Z) → U4_GA(U, V, W, Z, flatten_in_ga(cons(cons(U, V), W), X))
COUNT_IN_GA(cons(cons(U, V), W), Z) → FLATTEN_IN_GA(cons(cons(U, V), W), X)
FLATTEN_IN_GA(cons(atom(X), U), .(X, Y)) → U1_GA(X, U, Y, flatten_in_ga(U, Y))
FLATTEN_IN_GA(cons(atom(X), U), .(X, Y)) → FLATTEN_IN_GA(U, Y)
FLATTEN_IN_GA(cons(cons(U, V), W), X) → U2_GA(U, V, W, X, flatten_in_ga(cons(U, cons(V, W)), X))
FLATTEN_IN_GA(cons(cons(U, V), W), X) → FLATTEN_IN_GA(cons(U, cons(V, W)), X)
U4_GA(U, V, W, Z, flatten_out_ga(cons(cons(U, V), W), X)) → U5_GA(U, V, W, Z, count_in_ga(X, Z))
U4_GA(U, V, W, Z, flatten_out_ga(cons(cons(U, V), W), X)) → COUNT_IN_GA(X, Z)
count_in_ga(atom(X), s(0)) → count_out_ga(atom(X), s(0))
count_in_ga(cons(atom(X), Y), s(Z)) → U3_ga(X, Y, Z, count_in_ga(Y, Z))
count_in_ga(cons(cons(U, V), W), Z) → U4_ga(U, V, W, Z, flatten_in_ga(cons(cons(U, V), W), X))
flatten_in_ga(atom(X), .(X, [])) → flatten_out_ga(atom(X), .(X, []))
flatten_in_ga(cons(atom(X), U), .(X, Y)) → U1_ga(X, U, Y, flatten_in_ga(U, Y))
flatten_in_ga(cons(cons(U, V), W), X) → U2_ga(U, V, W, X, flatten_in_ga(cons(U, cons(V, W)), X))
U2_ga(U, V, W, X, flatten_out_ga(cons(U, cons(V, W)), X)) → flatten_out_ga(cons(cons(U, V), W), X)
U1_ga(X, U, Y, flatten_out_ga(U, Y)) → flatten_out_ga(cons(atom(X), U), .(X, Y))
U4_ga(U, V, W, Z, flatten_out_ga(cons(cons(U, V), W), X)) → U5_ga(U, V, W, Z, count_in_ga(X, Z))
U5_ga(U, V, W, Z, count_out_ga(X, Z)) → count_out_ga(cons(cons(U, V), W), Z)
U3_ga(X, Y, Z, count_out_ga(Y, Z)) → count_out_ga(cons(atom(X), Y), s(Z))
FLATTEN_IN_GA(cons(cons(U, V), W), X) → FLATTEN_IN_GA(cons(U, cons(V, W)), X)
FLATTEN_IN_GA(cons(atom(X), U), .(X, Y)) → FLATTEN_IN_GA(U, Y)
count_in_ga(atom(X), s(0)) → count_out_ga(atom(X), s(0))
count_in_ga(cons(atom(X), Y), s(Z)) → U3_ga(X, Y, Z, count_in_ga(Y, Z))
count_in_ga(cons(cons(U, V), W), Z) → U4_ga(U, V, W, Z, flatten_in_ga(cons(cons(U, V), W), X))
flatten_in_ga(atom(X), .(X, [])) → flatten_out_ga(atom(X), .(X, []))
flatten_in_ga(cons(atom(X), U), .(X, Y)) → U1_ga(X, U, Y, flatten_in_ga(U, Y))
flatten_in_ga(cons(cons(U, V), W), X) → U2_ga(U, V, W, X, flatten_in_ga(cons(U, cons(V, W)), X))
U2_ga(U, V, W, X, flatten_out_ga(cons(U, cons(V, W)), X)) → flatten_out_ga(cons(cons(U, V), W), X)
U1_ga(X, U, Y, flatten_out_ga(U, Y)) → flatten_out_ga(cons(atom(X), U), .(X, Y))
U4_ga(U, V, W, Z, flatten_out_ga(cons(cons(U, V), W), X)) → U5_ga(U, V, W, Z, count_in_ga(X, Z))
U5_ga(U, V, W, Z, count_out_ga(X, Z)) → count_out_ga(cons(cons(U, V), W), Z)
U3_ga(X, Y, Z, count_out_ga(Y, Z)) → count_out_ga(cons(atom(X), Y), s(Z))
FLATTEN_IN_GA(cons(cons(U, V), W), X) → FLATTEN_IN_GA(cons(U, cons(V, W)), X)
FLATTEN_IN_GA(cons(atom(X), U), .(X, Y)) → FLATTEN_IN_GA(U, Y)
FLATTEN_IN_GA(cons(cons(U, V), W)) → FLATTEN_IN_GA(cons(U, cons(V, W)))
FLATTEN_IN_GA(cons(atom(X), U)) → FLATTEN_IN_GA(U)
No rules are removed from R.
FLATTEN_IN_GA(cons(cons(U, V), W)) → FLATTEN_IN_GA(cons(U, cons(V, W)))
FLATTEN_IN_GA(cons(atom(X), U)) → FLATTEN_IN_GA(U)
POL(FLATTEN_IN_GA(x1)) = 2·x1
POL(atom(x1)) = x1
POL(cons(x1, x2)) = 2 + 2·x1 + x2
COUNT_IN_GA(cons(cons(U, V), W), Z) → U4_GA(U, V, W, Z, flatten_in_ga(cons(cons(U, V), W), X))
U4_GA(U, V, W, Z, flatten_out_ga(cons(cons(U, V), W), X)) → COUNT_IN_GA(X, Z)
COUNT_IN_GA(cons(atom(X), Y), s(Z)) → COUNT_IN_GA(Y, Z)
count_in_ga(atom(X), s(0)) → count_out_ga(atom(X), s(0))
count_in_ga(cons(atom(X), Y), s(Z)) → U3_ga(X, Y, Z, count_in_ga(Y, Z))
count_in_ga(cons(cons(U, V), W), Z) → U4_ga(U, V, W, Z, flatten_in_ga(cons(cons(U, V), W), X))
flatten_in_ga(atom(X), .(X, [])) → flatten_out_ga(atom(X), .(X, []))
flatten_in_ga(cons(atom(X), U), .(X, Y)) → U1_ga(X, U, Y, flatten_in_ga(U, Y))
flatten_in_ga(cons(cons(U, V), W), X) → U2_ga(U, V, W, X, flatten_in_ga(cons(U, cons(V, W)), X))
U2_ga(U, V, W, X, flatten_out_ga(cons(U, cons(V, W)), X)) → flatten_out_ga(cons(cons(U, V), W), X)
U1_ga(X, U, Y, flatten_out_ga(U, Y)) → flatten_out_ga(cons(atom(X), U), .(X, Y))
U4_ga(U, V, W, Z, flatten_out_ga(cons(cons(U, V), W), X)) → U5_ga(U, V, W, Z, count_in_ga(X, Z))
U5_ga(U, V, W, Z, count_out_ga(X, Z)) → count_out_ga(cons(cons(U, V), W), Z)
U3_ga(X, Y, Z, count_out_ga(Y, Z)) → count_out_ga(cons(atom(X), Y), s(Z))
COUNT_IN_GA(cons(cons(U, V), W), Z) → U4_GA(U, V, W, Z, flatten_in_ga(cons(cons(U, V), W), X))
U4_GA(U, V, W, Z, flatten_out_ga(cons(cons(U, V), W), X)) → COUNT_IN_GA(X, Z)
COUNT_IN_GA(cons(atom(X), Y), s(Z)) → COUNT_IN_GA(Y, Z)
flatten_in_ga(cons(cons(U, V), W), X) → U2_ga(U, V, W, X, flatten_in_ga(cons(U, cons(V, W)), X))
U2_ga(U, V, W, X, flatten_out_ga(cons(U, cons(V, W)), X)) → flatten_out_ga(cons(cons(U, V), W), X)
flatten_in_ga(cons(atom(X), U), .(X, Y)) → U1_ga(X, U, Y, flatten_in_ga(U, Y))
U1_ga(X, U, Y, flatten_out_ga(U, Y)) → flatten_out_ga(cons(atom(X), U), .(X, Y))
flatten_in_ga(atom(X), .(X, [])) → flatten_out_ga(atom(X), .(X, []))
COUNT_IN_GA(cons(cons(U, V), W)) → U4_GA(flatten_in_ga(cons(cons(U, V), W)))
U4_GA(flatten_out_ga(X)) → COUNT_IN_GA(X)
COUNT_IN_GA(cons(atom(X), Y)) → COUNT_IN_GA(Y)
flatten_in_ga(cons(cons(U, V), W)) → U2_ga(flatten_in_ga(cons(U, cons(V, W))))
U2_ga(flatten_out_ga(X)) → flatten_out_ga(X)
flatten_in_ga(cons(atom(X), U)) → U1_ga(X, flatten_in_ga(U))
U1_ga(X, flatten_out_ga(Y)) → flatten_out_ga(.(X, Y))
flatten_in_ga(atom(X)) → flatten_out_ga(.(X, []))
flatten_in_ga(x0)
U2_ga(x0)
U1_ga(x0, x1)
The following rules are removed from R:
COUNT_IN_GA(cons(atom(X), Y)) → COUNT_IN_GA(Y)
Used ordering: POLO with Polynomial interpretation [POLO]:
flatten_in_ga(cons(atom(X), U)) → U1_ga(X, flatten_in_ga(U))
U1_ga(X, flatten_out_ga(Y)) → flatten_out_ga(.(X, Y))
flatten_in_ga(atom(X)) → flatten_out_ga(.(X, []))
POL(.(x1, x2)) = x1 + x2
POL(COUNT_IN_GA(x1)) = x1
POL(U1_ga(x1, x2)) = 1 + 2·x1 + x2
POL(U2_ga(x1)) = x1
POL(U4_GA(x1)) = x1
POL([]) = 0
POL(atom(x1)) = 1 + 2·x1
POL(cons(x1, x2)) = 2·x1 + x2
POL(flatten_in_ga(x1)) = x1
POL(flatten_out_ga(x1)) = 2·x1
COUNT_IN_GA(cons(cons(U, V), W)) → U4_GA(flatten_in_ga(cons(cons(U, V), W)))
U4_GA(flatten_out_ga(X)) → COUNT_IN_GA(X)
flatten_in_ga(cons(cons(U, V), W)) → U2_ga(flatten_in_ga(cons(U, cons(V, W))))
U2_ga(flatten_out_ga(X)) → flatten_out_ga(X)
flatten_in_ga(x0)
U2_ga(x0)
U1_ga(x0, x1)
U1_ga(x0, x1)
COUNT_IN_GA(cons(cons(U, V), W)) → U4_GA(flatten_in_ga(cons(cons(U, V), W)))
U4_GA(flatten_out_ga(X)) → COUNT_IN_GA(X)
flatten_in_ga(cons(cons(U, V), W)) → U2_ga(flatten_in_ga(cons(U, cons(V, W))))
U2_ga(flatten_out_ga(X)) → flatten_out_ga(X)
flatten_in_ga(x0)
U2_ga(x0)
U4_GA(flatten_out_ga(X)) → COUNT_IN_GA(X)
POL(COUNT_IN_GA(x1)) = 2·x1
POL(U2_ga(x1)) = x1
POL(U4_GA(x1)) = 2·x1
POL(cons(x1, x2)) = x1 + x2
POL(flatten_in_ga(x1)) = x1
POL(flatten_out_ga(x1)) = 2 + 2·x1
COUNT_IN_GA(cons(cons(U, V), W)) → U4_GA(flatten_in_ga(cons(cons(U, V), W)))
flatten_in_ga(cons(cons(U, V), W)) → U2_ga(flatten_in_ga(cons(U, cons(V, W))))
U2_ga(flatten_out_ga(X)) → flatten_out_ga(X)
flatten_in_ga(x0)
U2_ga(x0)